(* # =================================================================== 
   # Introduction
   #
   # This work is the formalization of DPIA in Coq.
   #
   # This file is for the generation of matrix code, and the axioms used
   #
   #   has been proved in FDPIA_proof.v.
   #
   # The formalization of the translation consists of 
   #
   #   types, primitives, translators and rewrite rules and rewriting tactics.
   #
   # =================================================================== *)

Require Import Strings.String Reals List Ascii String Nat.
Require Export finType vector.
Set Implicit Arguments.
Import ListNotations.

(* *************************** Types *************************** *)

Inductive data : Set := 
  | num   : data
  | ary  : forall n, fle n -> data -> data 
  | tensor: data -> data.

Fixpoint exp (d:data) : Set :=
  match d with
  | num => R 
  | ary n d => vector (exp d) n
  | tensor d => (exp d) * (exp d)
  end.

Fixpoint exp_default (d:data) : exp d :=
  match d with
  | num => 0%R
  | ary n d => v_make n (exp_default d)
  | tensor d => (exp_default d, exp_default d)
  end.

Inductive path :=
  | Var : string -> path
  | AryIdx (n:nat) (i:fin n)  : path -> path
  | PairL : path -> path
  | PairR : path -> path.

Fixpoint acc (d:data) : Set :=
  match d with
  | num => path 
  | ary n d => vector (acc d) n
  | tensor d => (acc d) * (acc d)
  end.

Fixpoint acc' {d:data} (p:path) : acc d:=
  match d with
  | num => p:acc num
  | @ary n m d1 => mk_vec (fun i => acc' (AryIdx n (nat2fin n i) p))
  | tensor d1 => (acc' (PairL p),acc' (PairR p))
  end.

Fixpoint acc_default (d:data) : acc d :=
  match d with
  | num => Var ""
  | ary n d => v_make n (acc_default d)
  | tensor d => (acc_default d, acc_default d)
  end.

Notation " '{ n } " := (fle_self n) (at level 2).

(* *************************** Primitives *************************** *)

(* Primitives for Scalar Expression *)
Parameter negate: (exp num) -> (exp num).
Parameters add mul: (exp num) -> (exp num) -> (exp num).
Parameters zero one : exp num.

(* Primitives for Array Expression *)
Parameter mapSeq : forall {n:nat} {s t:data},
   ((exp s) -> (exp t)) -> (exp (ary '{n} s)) -> (exp (ary '{n} t)).
Parameter mapPar : forall {n:nat} {s t:data},
   ((exp s) -> (exp t)) -> (exp (ary '{n} s)) -> (exp (ary '{n} t)).
Parameter reduce : forall {n:nat} {s t:data},
   ((exp s)->(exp t)->(exp t))->(exp t)->(exp (ary '{n} s))->(exp t).
Parameter zip : forall {n:nat} {t:data},
   (exp (ary '{n} t)) -> (exp (ary '{n} t))->(exp (ary '{n} (tensor t))).
Parameter idx : forall {n:nat} {t:data},(exp (ary '{n} t)) -> fin n -> (exp t).
Parameter split : forall {t:data} {n m:nat},
   (exp (ary '{m*n} t)) -> (exp (ary '{m} (ary '{n} t))).
Parameter join : forall {t:data} {n m:nat},
  (exp (ary '{m} (ary '{n} t))) -> (exp (ary '{m*n} t)).

Notation " a |[ i ] " := (idx a i) (at level 2).

(* Primitives for Dual Expression *)
Parameter Pair : forall {t:data},(exp t) -> (exp t) -> (exp (tensor t)).
Parameter Fst : forall {t:data}, (exp (tensor t)) -> (exp t).
Parameter Snd : forall {t:data}, (exp (tensor t)) -> (exp t).

(* Primitives for Array Acceptor *)
Parameter zipAcc1 : forall {n:nat} {t:data},(acc (ary '{n} (tensor t))) -> acc (ary '{n} t).
Parameter zipAcc2 : forall {n:nat} {t:data},(acc (ary '{n} (tensor t))) -> acc (ary '{n} t).
Parameter idxAcc : forall {n:nat} {t:data}, acc (ary '{n} t) -> fin n -> acc t.
Parameter splitAcc : forall {n m:nat} {t:data}, acc (ary '{m} (ary '{n} t)) -> acc (ary '{m*n} t).
Parameter joinAcc : forall {n m:nat} {t:data}, acc (ary '{m*n} t) -> acc (ary '{m} (ary '{n} t)).

Notation " a |{ i } " := (idxAcc a i) (at level 2).

(* Primitives for Dual Acceptor *)
Parameter pairAcc1 : forall {t : data}, acc (tensor t) -> acc t.
Parameter pairAcc2 : forall {t : data}, acc (tensor t) -> acc t.

Definition cur {d d1:data} (f: exp d -> exp d -> exp d1):=
  fun (xy:exp (tensor d)) => f (Fst xy) (Snd xy).

(* Primitives for command *)
Inductive comm : Type := 
 | seq     : comm * comm -> comm
 | skip    : comm
 | assign  : forall {d:data}, (acc d) * (exp d) -> comm
 | new     : forall {d:data}, ((acc d) * (exp d) -> comm) -> comm
 | seqfor  : forall {n:nat}, (fin n -> comm) -> comm
 | parfor  : forall {n:nat} {d:data}, (acc (ary '{n} d)) ->
    (fin n -> acc d -> comm) -> comm.

Notation " p1 '; p2 " := (seq (p1,p2)) (right associativity,at level 65).
Notation " a |:= e " := (assign (a,e)) (at level 60).

(* ****************** Primitive Fusion Rules ****************** *)

Axiom mapPar_mapPar: forall [n:nat] [d1 d2 d3:data] 
  (f:exp d1 -> exp d2) (g: exp d2 -> exp d3) (v:exp (ary '{n} d1)),
  mapPar g (mapPar f v) = mapPar (fun i => g (f i)) v.

Axiom mapPar_join_split: forall [m n:nat] [d1 d2:data] (f:exp d1 -> exp d2) (v:exp (ary '{m*n} d1)),
  mapPar f v = join (mapPar (mapPar f) (split v)).

Axiom reduce_mapSeq: forall [n:nat] [d1 d2 d3:data] (g:exp d1 -> exp d2) 
    (f: exp d2 -> exp d3 -> exp d3) (i:exp d3)(v:exp (ary '{n} d1)),
  reduce f i (mapSeq g v) = reduce (fun x a => f (g x) a) i v.

Axiom join_split: forall (m n:nat) (d:data) (v: exp (ary '{m*n} d)),
  join (split v) = v.

Axiom split_join: forall (m n:nat) (d:data) (v: exp (ary '{m} (ary '{n} d))),
  split (join v) = v.

Axiom zip_mapPar: forall (d1 d2:data) (n:nat) (f g: exp d1 -> exp d2) (a b: exp (ary '{n} d1)),
  zip (mapPar f a) (mapPar g b) = mapPar (fun xy => (f (Fst xy),g (Snd xy)): exp (tensor d2)) (zip a b).

Lemma product_eq: forall (m n:nat) (a b: exp(ary '{m*n} num)),
  reduce add zero (mapPar (cur mul) (zip a b)) =
  reduce add zero(join (mapPar (mapPar (cur mul)) (split (zip a b)))).
Proof. intros. rewrite mapPar_join_split. auto. Qed.

(* ****************** Intermediate Imperative Micros ****************** *)

Definition reducel [n:nat] [d1 d2:data]
   (f : exp d1 -> exp d2 -> acc d2 -> comm) (init : exp d2)
   (xs : exp (ary '{n} d1)) (c : exp d2 -> comm) :=
  new (fun ac =>
    let (vw, vr) := ac in 
       (vw |:= init) '; 
       (seqfor (fun i => f (xs |[i]) vr vw)) ';
        c vr).

Definition mapSeql [n:nat] [d1 d2:data] (f:exp d1 -> acc d2 -> comm) (v:exp(ary '{n} d1)) (out:acc(ary '{n} d2)):=
  seqfor (fun i  => f v|[i] out|{i}).

Definition mapParl [n:nat] [d1 d2:data] (f:exp d1 -> acc d2 -> comm) (v:exp(ary '{n} d1)) (out:acc(ary '{n} d2)):=
  parfor out (fun i o => f v|[i] o).

(* ************ Translators from Functional to Imperative ************* *)

Definition Atrans {d:data} (a:acc d) (e:exp d) :=  assign (a,e).

Notation " A{ e , a }  " := (Atrans a e) (at level 60).

Definition Ctrans {d:data} (e:exp d) (c: (exp d) -> comm):= c e.

Notation " C{ e , c } " := (Ctrans e c) (at level 60).

Hint Unfold Atrans Ctrans.

Section Axiom_used.

Axiom reducel_equiv: forall n d1 d2 f (i:exp d2) (a:path) (e:exp (ary '{n} d1)) ,
  acc' a |:= reduce f i e =
new
  (fun ac : acc d2 * exp d2 =>
   let (vw, vr) := ac in
   vw |:= i
   '; seqfor
        (fun i0 : fin n => vw |:= f e |[ i0] vr)
      '; acc' a |:= vr).

Axiom assign_ary_par: forall (n : nat) (d : data) (a : path) (x : exp (ary '{ n} d)),
  acc' a |:= x =
  parfor (acc' a) (fun (i : fin n) (o : acc d) => o |:= x |[ i]).

Axiom assign_tensor: forall (d : data) (a : path) (x : exp (tensor d)),
  acc' a |:= x 
  = pairAcc1 (acc' a) |:= Fst x '; pairAcc2 (acc' a) |:= Snd x.

Axiom assign_pair: forall (d : data) (e1 e2 : exp d) (a : path),
  acc' a |:= Pair e1 e2 
  = pairAcc1 (acc' a) |:= e1 '; pairAcc2 (acc' a) |:= e2.

Axiom mapSeq_equiv : forall (n : nat) (d1 d2 : data) (f : exp d1 -> exp d2) (v:exp (ary '{n} d1)) (a :path),
  acc' a |:= mapSeq f v  = seqfor (fun i : fin n => (acc' a)|{i} |:= f v|[i]).

Axiom mapPar_equiv : forall (n : nat) (d1 d2 : data) (f : exp d1 -> exp d2) (v:exp (ary '{n} d1)) (a : path),
  acc' a |:= mapPar f v  = parfor (acc' a) (fun (i : fin n) o => o |:= f v|[i]).

Axiom new_equiv: forall d c (e1:exp d),
  new (fun tmp => let (a,e2):= tmp in seq (assign (a,e1), c e2)) = c e1.

Axiom zip_equiv : forall n d (a: path) (e1 e2:exp(ary '{n} d)), 
  acc' a |:= zip e1 e2 
  = zipAcc1 (acc' a) |:= e1 '; zipAcc2 (acc' a) |:= e2.

Axiom split_equiv: forall (n m : nat) (d : data) (e : exp (ary '{ m * n} d)) (a : path),
  acc' a |:= split e = splitAcc (acc' a) |:= e.

Axiom join_equiv: forall (n m : nat) (d : data) (e : exp (ary '{ m} (ary '{ n} d))) (a : path),
  acc' a |:= join e = joinAcc (acc' a) |:= e.

Axiom reducel_equiv2:forall (n : nat) (d1 d2 : data) (f : exp d1 -> exp d2 -> exp d2) 
  (i : exp d2) (e : exp (ary '{ n} d1)) (c : exp d2 -> comm),
  c (reduce f i e) =
  new (fun ac : acc d2 * exp d2 =>
   let (vw, vr) := ac in vw |:= i '; 
   seqfor (fun i0 : fin n => vw |:= f e |[ i0] vr) '; c vr).

End Axiom_used.

(* ************* Rewrite Rules from Functional to Imperative ************* *)

Section RewriteRules.

Lemma Avar_num: forall (a:path) (e: exp num),
  A{ e, acc' a} = acc' a |:= e.
Proof. auto. Qed.

Lemma Avar_ary:forall (n:nat) (d:data) (a:path) (x:exp (ary '{n} d)),
  A{ x , acc' a } = mapParl (fun x a => a |:= x) x (acc' a).
Proof. autounfold. unfold mapParl. intros. apply assign_ary_par. Qed.

Lemma Avar_tensor: forall (d:data) (a:path)(x:exp (tensor d)),
  A{ x , acc' a } = pairAcc1 (acc' a) |:= Fst x '; pairAcc2 (acc' a) |:= Snd x.
Proof. autounfold. intros. apply assign_tensor. Qed.

Lemma Aneg : forall (a:path) (e:exp num),
  A{ negate e , acc' a } = C{ e , fun (x:exp num) => acc' a |:= negate x}.
Proof. auto. Qed.

Lemma Aadd : forall (a:path) (e1 e2:exp num) ,
  A{ add e1 e2 ,acc' a } = C{ e1 , fun x => C{ e2 , fun y => acc' a|:= add e1 e2}}.
Proof. auto. Qed.

Lemma Aadd1 :
  (fun e1 e2 a => A{ add e1 e2 ,a}) 
  = (fun e1 e2 a => C{ e1 , fun x => C{ e2 , fun y => a|:= add x y}}).
Proof. auto. Qed.

Lemma Amul : forall (a:path) (e1 e2:exp num),
  A{mul e1 e2 , acc' a } = C{ e1 ,fun x => C{ e2 , fun y => acc' a|:= mul e1 e2 }}.
Proof. auto. Qed.

Lemma AmapSeq : forall (n:nat) (d1 d2:data) (f:exp d1 -> exp d2)
  (e: exp (ary '{n} d1)) (a:path), 
  A{ mapSeq f e ,acc' a} = C{ e , fun x => mapSeql (fun x o => A{f x,o}) x (acc' a)}.
Proof.
  autounfold. intros. unfold mapSeql. rewrite mapSeq_equiv. auto.
Qed.

Lemma AmapPar : forall (n:nat) (d1 d2:data) (f:exp d1 -> exp d2)
  (e: exp (ary '{n} d1)) (a: path), 
  A{ mapPar f e , acc' a} = C{ e , fun x => mapParl (fun x o => A{f x,o}) x (acc' a)}.
Proof.
  autounfold. intros. rewrite mapPar_equiv. unfold mapParl. auto.
Qed.

Lemma Areduce : forall (n:nat) (d1 d2 : data)  
  (f:exp d1 -> exp d2 -> exp d2) (i:exp d2) (e:exp (ary '{n} d1)) (a:path),
  A{ reduce f i e , acc' a } = C{ e , fun x => 
    C{ i , fun y => reducel 
      (fun x' => (fun y' => (fun o => A{f x' y' , o})))
        y x (fun r => A{r , acc' a}) }}.
Proof. autounfold. unfold reducel. intros. rewrite reducel_equiv. auto. Qed.

Lemma Azip: forall (n:nat) (d:data) (e1 e2:exp(ary '{n} d))(a: path) ,
  A{zip e1 e2,acc' a} = A{e1,zipAcc1 (acc' a)}';A{e2,zipAcc2 (acc' a)}.
Proof. autounfold. intros. rewrite zip_equiv. auto. Qed.

Lemma Asplit: forall(n m:nat) (d:data)
  (e: exp(ary '{m*n} d)) (a: path),
  A{split e,acc' a} = A{e,splitAcc (acc' a)}.
Proof. autounfold. intros. apply split_equiv. Qed.

Lemma Ajoin: forall (n m:nat) (d:data) (e: exp (ary '{m} (ary '{n} d))) (a: path),
  A{join e,acc' a} = A{e,joinAcc (acc' a)}.
Proof. autounfold. intros. apply join_equiv. Qed.

Lemma Apair : forall (d:data)(e1 e2: exp d) (a:path) ,
  A{ Pair e1 e2 , acc' a } = A{ e1 , pairAcc1 (acc' a) } '; A{ e2 , pairAcc2 (acc' a) }.
Proof. autounfold. intros. apply assign_pair. Qed.

Lemma Afst: forall (d:data)(e:exp(tensor d))(a:path) ,
  A{ Fst e , acc' a } = C{ e , fun x=> acc' a|:= Fst x }.
Proof. autounfold. auto. Qed.

Lemma Asnd: forall (d:data)(e:exp(tensor d))(a:path) ,
  A{ Snd e , acc' a } = C{ e , fun x=> acc' a|:= Snd x }.
Proof. autounfold. auto. Qed.

Lemma Cvar: forall (d:data) (e: exp d) (c: exp d -> comm)  ,
  C{ e , c} = c e.
Proof. auto. Qed.

Lemma Cneg: forall (e:exp num) (c : exp num -> comm) ,
  C{ negate e , c } = C{ e , fun x => c (negate x) }.
Proof. auto. Qed.

Lemma Cadd: forall (e1 e2 : exp num) (c : exp num -> comm) ,
  C{ add e1 e2 , c } = 
  C{ e1 , fun x => C{ e2 , fun y => c (add x y) }}.
Proof. auto. Qed.

Lemma Cmul: forall (e1 e2 : exp num) (c : exp num -> comm) ,
  C{ mul e1 e2 , c } = 
  C{ e1 , fun x => C{ e2 , fun y => c (mul x y) }}.
Proof. auto. Qed.

Lemma CmapSeq: forall (n:nat)(d1 d2:data) (f:exp d1 -> exp d2)
   (e:exp (ary '{n} d1)) (c:exp (ary '{n} d2) -> comm)  ,
  C{ mapSeq f e , c } = new (fun tmp => let (a,e2):= tmp in
    A{ mapSeq f e , a } '; c e2).
Proof. intros. autounfold. rewrite new_equiv. auto. Qed.

Lemma CmapPar: forall (n:nat)(d1 d2:data) (f:exp d1 -> exp d2)
   (e:exp (ary '{n} d1)) (c:exp (ary '{n} d2) -> comm)  ,
  C{ mapPar f e , c } = new (fun tmp => let (a,e2):= tmp in
    A{ mapPar f e , a } '; c e2).
Proof. intros. autounfold. rewrite new_equiv. auto. Qed.

Lemma Creduce: forall (n:nat) (d1 d2:data)
   (f:exp d1 -> exp d2 -> exp d2) (i:exp d2) (e:exp (ary '{n} d1))
   (c: exp d2 -> comm),
  C{ reduce f i e , c} = 
  C{ e , fun x  => C{ i , fun y => reducel ( fun x' y' o => A{f x' y', o } ) y x c }}.
Proof. autounfold. unfold reducel. intros. apply reducel_equiv2. Qed.

Lemma Czip: forall (n:nat) (d:data) (e1 e2:exp(ary '{n} d)) (c: exp(ary '{n} (tensor d)) -> comm),
  C{ zip e1 e2 , c } = C{ e1 , fun x => C{ e2 , fun y => c (zip x y)}}.
Proof. intros. autounfold. auto. Qed.

Lemma Csplit: forall (m n:nat) (d:data) (e: exp(ary '{m*n} d)) (c: exp (ary '{m} (ary '{n} d)) -> comm),
  C{ split e , c } = C{ e , fun x => c (split x)}.
Proof. intros. autounfold. auto. Qed. 

Lemma Cjoin: forall (m n:nat) (d:data) (e: exp(ary '{m} (ary '{n} d))) (c: exp (ary '{m*n} d) -> comm),
  C{ join e , c } = C{ e , fun x => c (join x) }.
Proof. intros. autounfold. auto. Qed.

Lemma Cpair : forall (d:data)(e1:exp d) (e2:exp d)
  (c: exp (tensor d) -> comm) ,
  C{ @Pair d e1 e2 , c } =
  C{ e1 , fun x => C{ e2 , fun y => c (@Pair d x y) }}.
Proof. auto. Qed.

Lemma Cfst : forall (d:data) (e:exp (tensor d)) (c: exp d -> comm) ,
  C{ @Fst d e , c} = C{e , fun x => c (@Fst d x) }.
Proof. auto. Qed.

Lemma Csnd : forall (d:data) (e:exp (tensor d)) (c: exp d -> comm) ,
  C{ @Snd d e , c} = C{e , fun x => c (@Snd d x) }.
Proof. auto. Qed.

End RewriteRules.

(* ************* Rewrite Rules from Imperative to OpenMP C ************* *)

Section CodeGen_OpenMP.

Open Scope string_scope.

(* generate C type declaration. *)
Fixpoint CodeGen_data (d:data) s: string :=
  match d with
   | num => "float "++ s
   | ary n d => (CodeGen_data d (s++"["++(writeNat n)++"]") )
   | tensor d => "
struct {
 "++ (CodeGen_data d s)++" x1; 
 "++ (CodeGen_data d s)++" x2;
} "
  end.

Inductive Vpath := Aidx (i:nat) | Sacc (p:string).

Definition pslist := list Vpath.

(* convert a var to be a var of nat type. *)
Parameter str2nat : string -> nat.
Coercion str2nat : string >-> nat.

Parameter CodeGen_comm :  comm -> nat -> string.
Parameter CodeGen_acc   : 
  forall {d:data} , pslist -> acc d -> string.
Parameter CodeGen_exp   : 
  forall {d:data} , pslist -> exp d -> string.

Parameter vrd : forall {d:data}, string -> exp d.

Fixpoint cnt_var (c:comm):=
  match c with
  | seq (c1,c2) => cnt_var c1 + cnt_var c2
  | skip => 0
  | assign ac => 0
  | @new t p => 1+ cnt_var(p (acc' (Var ""),vrd ""))
  | @seqfor n p => 1 + cnt_var(p (nat2fin n 0))
  | @parfor n t a p =>1 + cnt_var (p (nat2fin n 0) (acc' (Var ""))) 
  end. 

Lemma cnt_seq: forall (c1 c2:comm),
  cnt_var (c1 '; c2) = cnt_var c1 + cnt_var c2.
Proof. intros. simpl. auto. Qed.

Lemma cnt_skip : cnt_var skip = 0.
Proof. simpl. auto. Qed.

Lemma cnt_assign: forall (d:data) a,
   cnt_var (@assign d a) = 0.
Proof. simpl. auto. Qed.

Lemma cnt_new : forall (t:data) p,
  cnt_var (@new t p) = 1 + cnt_var (p (acc' (Var ""),vrd "" )).
Proof. auto. Qed.

Lemma cnt_seqfor: forall (n:nat) p ,
  cnt_var(@seqfor n p) = 1+ cnt_var (p (nat2fin n 0)).
Proof. auto. Qed.

Lemma cnt_parfor: forall (n:nat) (t:data) a p,
  cnt_var (@parfor n t a p) = 1+ cnt_var (p (nat2fin n 0)(acc' (Var ""))) .
Proof. simpl. auto. Qed.

Definition vstr (cnt:nat) : string := "v"++(writeNat cnt ).
Definition istr (cnt:nat) : string := "i"++(writeNat cnt ).

Fixpoint applyps (v:string) (ps:pslist) : string :=
  match ps with
   | nil => v
   | (Aidx i)::tl => applyps (v ++"["++(writeNat i)++"]") tl 
   | (Sacc p)::tl => applyps (v++p) tl
  end.

Fixpoint pr_path (p:path): string :=
  match p with
  | Var x => x
  | AryIdx n i p => pr_path p ++ "[" ++ (writeNat i) ++ "]"
  | PairL p => pr_path p ++ ".x1"
  | PairR p => pr_path p ++ ".x2"
  end.

Parameter CGskip :  forall (cnt:nat), 
  CodeGen_comm skip cnt = " /* skip */ ".

Parameter CGseq  : forall (p1 p2:comm) (cnt:nat),
   CodeGen_comm (p1 '; p2) cnt  = 
  (CodeGen_comm p1 cnt)++"
"++(CodeGen_comm p2 (cnt_var p1 + cnt)).

Parameter CGassign : forall (a:acc num) (e:exp num) (cnt:nat), 
   CodeGen_comm (a |:= e) cnt = 
   (CodeGen_acc [] a) ++" = "
   ++(CodeGen_exp [] e)++" ;". 

Parameter CGassign_ary: forall (d:data) (n:nat) 
  (a:acc(ary '{n} d))(e:exp(ary '{n} d))(cnt:nat),
  CodeGen_comm (a |:= e) cnt = 
  CodeGen_comm (seqfor (fun i=> a|{i} |:= e |[i])) cnt. 

Parameter CGnew : forall (d:data) (p:acc d * exp d -> comm) (cnt:nat), 
  CodeGen_comm (new p) cnt =
  (CodeGen_data d) (vstr cnt) ++";
"
  ++ (CodeGen_comm 
  (p(acc'(Var (vstr cnt)) ,vrd (vstr cnt) )) (cnt+1)).

Parameter str2fin : forall (n:nat), string -> fin n.

Parameter CGfor : forall (n:nat) (p:fin n -> comm) (cnt:nat),
  CodeGen_comm (seqfor p) cnt =
"for(int "++(istr cnt)++"=0; "++(istr cnt)++"<"
    ++(writeNat n)++"; "++(istr cnt)++" += 1) 
  { " ++ (CodeGen_comm (p (str2fin n(istr cnt))) (cnt+1)) ++ "}".

Parameter CGparfor : forall (n:nat) (d:data) (a:acc (ary '{n} d))
   (p:fin n -> acc d -> comm) (cnt:nat),
  CodeGen_comm (parfor a p) cnt =
"#pragma omp parallel for
for (int "++(istr cnt)++"=0; "++(istr cnt)++" < "
    ++(writeNat n)++"; "++(istr cnt)++" += 1) 
  { " ++ (CodeGen_comm 
     (p (str2fin n (istr cnt)) 
    (a|{(str2fin n (istr cnt))})) (cnt+1)) ++ "}".

Axiom CGaccvar : forall (d:data) (x:path) (ps:pslist), 
   @CodeGen_acc d ps (acc' x) = 
   applyps (pr_path x) ps.

Axiom CGidxAcc : forall (d:data) (n:nat) (a:acc (ary '{n} d)) 
  (i:fin n) (ps:pslist),
  CodeGen_acc ps (a |{i}) = CodeGen_acc (Aidx i :: ps) a.

Axiom CGsplitAcc : forall (d:data) (n m: nat) (a:acc (ary '{m} (ary '{n} d)))(i:nat) (ps:pslist),
  CodeGen_acc (Aidx i::ps) (splitAcc a) =
  CodeGen_acc (Aidx (i / m)::Aidx (i mod m)::ps) a.

Axiom CGjoinAcc : forall (d:data) (n m: nat) (a:acc (ary '{m*n} d))
  (i j:nat) (ps:pslist),
  CodeGen_acc (Aidx i::Aidx j::ps) (joinAcc a) =
  CodeGen_acc (Aidx (i * n + j)::ps) a.

Axiom CGpairAcc1 : forall (d:data) (a: acc (tensor d)) (ps:pslist),
  CodeGen_acc ps (pairAcc1 a) =
  CodeGen_acc (Sacc ".x1"::ps) a.

Axiom CGpairAcc2 : forall (d:data) (a: acc (tensor d)) (ps:pslist),
  CodeGen_acc ps (pairAcc2 a) =
  CodeGen_acc (Sacc ".x2"::ps) a.

Axiom CGzipAcc1 : forall (n:nat) (d:data) 
  (a: acc (ary '{n} (tensor d))) (ps:pslist) (i:nat),
  CodeGen_acc (Aidx i::ps) (zipAcc1 a) =
  CodeGen_acc (Aidx i::Sacc ".x1"::ps) a.

Axiom CGzipAcc2 : forall (n:nat) (d:data) 
  (a: acc (ary '{n} (tensor d))) (ps:pslist) (i:nat),
  CodeGen_acc (Aidx i::ps) (zipAcc2 a) =
  CodeGen_acc (Aidx i::Sacc ".x2"::ps) a.

(* r-values. *)

Parameter CGexpvar : forall (d:data) (x:string) (ps:pslist), 
   @CodeGen_exp d ps (vrd x) = applyps x ps.

Parameter CGneg : forall (e:exp num),
  CodeGen_exp [] (negate e) = "(- "++(CodeGen_exp [] e)++")".

Parameter CGadd : forall (e1 e2 : exp num),
  CodeGen_exp [] (add e1 e2) =
  "("++(CodeGen_exp [] e1)++
  " + "++(CodeGen_exp [] e2)++")".

Axiom CGmul : forall (e1 e2 : exp num),
  CodeGen_exp [] (mul e1 e2) =
  "("++(CodeGen_exp [] e1)++
  " * "++(CodeGen_exp [] e2)++")".

Axiom CGzip1 : forall (n:nat) (d:data) (e1:exp (ary '{n} d)) (e2:exp (ary '{n} d)) (i :nat) (ps:pslist),
  CodeGen_exp (Aidx i::Sacc ".x1"::ps)(zip e1 e2) = 
  CodeGen_exp (Aidx i::ps) e1.

Axiom CGzip2 : forall (n:nat) (d:data) 
  (e1:exp (ary '{n} d)) (e2:exp (ary '{n} d)) (i :nat) (ps:pslist),
  CodeGen_exp (Aidx i::Sacc ".x2"::ps)(zip e1 e2) = 
  CodeGen_exp (Aidx i::ps) e2.

Axiom CGsplit : forall (d:data) (n m: nat) (e:exp (ary '{m*n} d))
  (i j:nat) (ps:pslist),
  CodeGen_exp (Aidx i::Aidx j::ps) (split e) =
  CodeGen_exp (Aidx (i*n+j)::ps) e.

Axiom CGjoin : forall (d:data) (n m: nat) (e:exp (ary '{m} (ary '{n} d)))
  (i:nat) (ps:pslist),
  CodeGen_exp (Aidx i::ps) (join e) =
  CodeGen_exp (Aidx (i / m)::Aidx (i mod m)::ps) e.

Parameter CGpair1 : forall (n m:nat) (d:data) 
  (e1:exp d) (e2:exp d) (ps:pslist),
  CodeGen_exp (Sacc ".x1"::ps) (Pair e1 e2) = 
  CodeGen_exp ps e1.

Parameter CGpair2 : forall (n m:nat) (d:data) 
  (e1:exp d) (e2:exp d) (ps:pslist),
  CodeGen_exp (Sacc ".x2"::ps) (Pair e1 e2) = 
  CodeGen_exp ps e1.

Parameter CGfst : forall (d:data) (e: exp (tensor d)) (ps:pslist),
  CodeGen_exp ps (Fst e) =
  CodeGen_exp (Sacc ".x1"::ps) e.

Parameter CGsnd : forall (d:data) (e: exp (tensor d)) (ps:pslist),
  CodeGen_exp ps (Snd e) =
  CodeGen_exp (Sacc ".x2"::ps) e.

Parameter wtStrNat : forall (s:string), writeNat (str2nat s) = s.

Parameter CGidx : forall (d:data) (n:nat) (e:exp (ary '{n} d)) 
  (i: fin n) (ps:pslist),
  CodeGen_exp ps (idx e i) =
  CodeGen_exp (Aidx i::ps) e.

End CodeGen_OpenMP.

(* **************************** Rewriting Tactics **************************** *)

Open Scope string_scope.

Axiom writeNat_nat2fin: forall n m, writeNat(nat2fin n m) = writeNat m.

Axiom writeNat_str2fin: forall n (s:string), writeNat (str2fin n s) = s.

Axiom writeNat_add: forall (m n:nat),writeNat (m+n) = writeNat m ++ "+" ++ writeNat n.

Axiom writeNat_mul: forall (m n:nat),writeNat (m*n) = writeNat m ++ "*" ++ writeNat n.

Axiom writeNat_div: forall (m n:nat),writeNat (m/n) = writeNat m ++ "/" ++ writeNat n.

Axiom writeNat_mod: forall (m n:nat),writeNat (m mod n) = writeNat m ++ "%" ++ writeNat n.

Axiom acc'_idx: forall (p:path) (n:nat) (d:data) (i:fin n),
  (@acc' (ary '{n} d) p) |{i} = @acc' d (AryIdx n i p).

Ltac hypRewrite :=
  match goal with
  | [ H: writeNat ?m = _ |- _] => rewrite ?H;clear H
  end.

Ltac hypUnfold :=
  match goal with
  | [ H:= vrd _ |- _] => (unfold H;clear H)
  end.

Ltac strnat_simpl:=
  simpl;
  repeat (rewrite ?writeNat_nat2fin,?writeNat_str2fin,?writeNat_add,
  ?writeNat_mul,?writeNat_div,?writeNat_mod,?wtStrNat); simpl;repeat hypRewrite.


Ltac cnt_simpl:=
  rewrite ?cnt_seq,?cnt_skip,?cnt_assign,?cnt_new,?cnt_seqfor,?cnt_parfor.

Ltac Asimpl1 :=
  rewrite ?AmapSeq,?AmapPar,?Areduce;
  try unfold mapParl,mapSeql,reducel.

Ltac Asimpl2 :=
  rewrite ?Azip,?Asplit,?Ajoin,?Afst,?Asnd;
  rewrite ?Aadd,?Amul,?Avar_ary,?Avar_tensor,?Avar_num.

Ltac Csimpl1:=
  repeat (rewrite ?CmapPar,?CmapSeq,?Creduce);
  try unfold mapParl,mapSeql,reducel.

Ltac Csimpl2 :=
  rewrite ?Czip,?Csplit,?Cjoin,?Cfst,?Csnd;
  rewrite ?Cmul,?Cadd.

Ltac CGsimpl:=
  rewrite ?CGskip,?CGseq,?CGassign,?CGassign_ary,?CGnew,?CGfor,?CGparfor,?acc'_idx;
  repeat cnt_simpl;
  rewrite ?CGzip1,?CGzip2,?CGsplit,?CGjoin,?CGfst,?CGsnd;
  rewrite ?CGidxAcc,?CGidx,?CGmul,?CGadd,?CGaccvar,?CGexpvar.

Ltac Allsimpl:=
  Asimpl1;Asimpl2;Csimpl1;Csimpl2;CGsimpl. 

Ltac Translate :=
  unfold cur;
  repeat hypUnfold; 
  repeat (repeat Allsimpl;rewrite ?Cvar);
  repeat strnat_simpl. 




